T:Type, x:T. (x ! nil)  False 

latex

Definitions	P  Q, False, A, AB, , x:A. B(x), P & Q, A & B, x:A. B(x), t  T, ||as||, l[i], Prop, P  Q, P  Q, (x ! l)
Lemmas	length wf2, select wf, nat wf, false wf